Inference at * 1 1 0 
Iof proof for Lemma connex functionality wrt implies:



1. T : Type
2. R : TT
3. R' : TT
4. x, y:T. {R(x,y)  R'(x,y)}
5. x, y:T. R(x,y)  R(y,x)
6. x : T
7. y : T
  R'(x,y)  R'(y,x) 

latex

 by PERMUTE{1:n,
 by PERMUTE{1:n,
 by PERMUTE{2:n,
 by PERMUTE{3:n,
 by PERMUTE{4:n,
 by PERMUTE{5:n,
 by PERMUTE{5:n,
 by PERMUTE{6:n,
 by PERMUTE{7:n,
 by PERMUTE{8:n,
 by PERMUTE{9:n,
 by PERMUTE{10:n,
 by PERMUTE{11:n,
 by PERMUTE{12:n,
 by PERMUTE{13:n,
 by PERMUTE{14:n,
 by PERMUTE{14:n,
 by PERMUTE{13:n,
 by PERMUTE{5:n,
 by PERMUTE{1:n,
 by PERMUTE{15:n} 

latex

 1: .....wf..... NILNIL

 1:   T  Type
 2: .....wf..... NILNIL

 2:   (x.y:T. R(x,y)  R(y,x))  T
 3: .....wf..... NILNIL

 3:   (x.y:T. R'(x,y)  R'(y,x))  T
 4: .....wf..... NILNIL

 4:   T = T
 5: .....wf..... NILNIL

 5: 8. T
 5:   T  Type
 6: .....wf..... NILNIL

 6: 8. z : T
 6:   (y.R(z,y)  R(y,z))  T
 7: .....wf..... NILNIL

 7: 8. z : T
 7:   (y.R'(z,y)  R'(y,z))  T
 8: .....wf..... NILNIL

 8: 8. T
 8:   T = T
 9: .....wf..... NILNIL

 9: 8. z : T
 9: 9. z1 : T
 9:   R(z,z1)  
 10: .....wf..... NILNIL

 10: 8. z : T
 10: 9. z1 : T
 10:   R'(z,z1)  
 11: .....wf..... NILNIL

 11: 8. z : T
 11: 9. z1 : T
 11:   R(z1,z)  
 12: .....wf..... NILNIL

 12: 8. z : T
 12: 9. z1 : T
 12:   R'(z1,z)  
 13: .....wf..... NILNIL

 13: 8. z : T
 13: 9. T
 13:   z  T
 14: .....wf..... NILNIL

 14: 8. T
 14: 9. z1 : T
 14:   z1  T
 15: 

 15: 5. x, y:T. R'(x,y)  R'(y,x)
 15: 6. x : T
 15: 7. y : T
 15:   R'(x,y)  R'(y,x)
 .

Definitions	t  T, x.A(x), f(a), s = t, P  Q, x(s1,s2), , x:AB(x), Type, x(s), P  Q, x. t(x), {T}, x:A. B(x)
Lemmas	or functionality wrt implies, all functionality wrt implies